0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 182 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 256 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 22 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 9 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 MRRProof (⇔, 143 ms)
↳36 QDP
↳37 DependencyGraphProof (⇔, 0 ms)
↳38 QDP
↳39 UsableRulesProof (⇔, 0 ms)
↳40 QDP
↳41 QReductionProof (⇔, 0 ms)
↳42 QDP
↳43 QDPSizeChangeProof (⇔, 0 ms)
↳44 YES
↳45 PiDP
↳46 UsableRulesProof (⇔, 0 ms)
↳47 PiDP
↳48 PiDPToQDPProof (⇒, 4 ms)
↳49 QDP
↳50 QDPOrderProof (⇔, 320 ms)
↳51 QDP
↳52 DependencyGraphProof (⇔, 0 ms)
↳53 TRUE
MERGESORTF_IN_GA(.(X1, .(X2, [])), X3) → U10_GA(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U10_GA(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U11_GA(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U11_GA(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U12_GA(X1, X2, X3, mergeB_in_gga(X4, X5, X3))
U11_GA(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → MERGEB_IN_GGA(X4, X5, X3)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U1_GGA(X1, X2, X3, X4, X5, leC_in_gg(X1, X3))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEC_IN_GG(X1, X3)
LEC_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U3_GGA(X1, X2, X3, X4, X5, mergeB_in_gga(X2, .(X3, X4), X5))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4), X5)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U4_GGA(X1, X2, X3, X4, X5, gtD_in_gg(X1, X3))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTD_IN_GG(X1, X3)
GTD_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U6_GGA(X1, X2, X3, X4, X5, mergeB_in_gga(.(X1, X2), X4, X5))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4, X5)
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U13_GA(X1, X2, X3, X4, X5, splitE_in_gaa(X4, X6, X7))
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → SPLITE_IN_GAA(X4, X6, X7)
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → U9_GAA(X1, X2, X3, X4, splitE_in_gaa(X2, X4, X3))
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITE_IN_GAA(X2, X4, X3)
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U14_GA(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U15_GA(X1, X2, X3, X4, X5, mergesortF_in_ga(.(X1, .(X3, X7)), X8))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)), X8)
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U17_GA(X1, X2, X3, X4, X5, mergesortF_in_ga(.(X2, X6), X9))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6), X9)
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U19_GA(X1, X2, X3, X4, X5, mergeB_in_gga(X8, X9, X5))
U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → MERGEB_IN_GGA(X8, X9, X5)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MERGESORTF_IN_GA(.(X1, .(X2, [])), X3) → U10_GA(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U10_GA(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U11_GA(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U11_GA(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U12_GA(X1, X2, X3, mergeB_in_gga(X4, X5, X3))
U11_GA(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → MERGEB_IN_GGA(X4, X5, X3)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U1_GGA(X1, X2, X3, X4, X5, leC_in_gg(X1, X3))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEC_IN_GG(X1, X3)
LEC_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U3_GGA(X1, X2, X3, X4, X5, mergeB_in_gga(X2, .(X3, X4), X5))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4), X5)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U4_GGA(X1, X2, X3, X4, X5, gtD_in_gg(X1, X3))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTD_IN_GG(X1, X3)
GTD_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U6_GGA(X1, X2, X3, X4, X5, mergeB_in_gga(.(X1, X2), X4, X5))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4, X5)
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U13_GA(X1, X2, X3, X4, X5, splitE_in_gaa(X4, X6, X7))
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → SPLITE_IN_GAA(X4, X6, X7)
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → U9_GAA(X1, X2, X3, X4, splitE_in_gaa(X2, X4, X3))
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITE_IN_GAA(X2, X4, X3)
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U14_GA(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U15_GA(X1, X2, X3, X4, X5, mergesortF_in_ga(.(X1, .(X3, X7)), X8))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)), X8)
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U17_GA(X1, X2, X3, X4, X5, mergesortF_in_ga(.(X2, X6), X9))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6), X9)
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U19_GA(X1, X2, X3, X4, X5, mergeB_in_gga(X8, X9, X5))
U18_GA(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → MERGEB_IN_GGA(X8, X9, X5)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITE_IN_GAA(X2, X4, X3)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
SPLITE_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITE_IN_GAA(X2, X4, X3)
SPLITE_IN_GAA(.(X1, X2)) → SPLITE_IN_GAA(X2)
From the DPs we obtained the following set of size-change graphs:
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4), X5)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4, X5)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U2_GGA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4), X5)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4, X5)
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U2_GGA(X1, X2, X3, X4, lecC_in_gg(X1, X3))
U2_GGA(X1, X2, X3, X4, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U5_GGA(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4)
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
gtcD_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U2_GGA(X1, X2, X3, X4, lecC_in_gg(X1, X3))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
POL(.(x1, x2)) = 1 + 2·x1 + x2
POL(0) = 0
POL(MERGEB_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U25_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U26_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U2_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + 2·x3 + 2·x4 + x5
POL(U5_GGA(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(gtcD_in_gg(x1, x2)) = 1 + x1 + x2
POL(gtcD_out_gg(x1, x2)) = x1 + x2
POL(lecC_in_gg(x1, x2)) = 2·x1 + 2·x2
POL(lecC_out_gg(x1, x2)) = 2·x1 + 2·x2
POL(s(x1)) = 2·x1
U2_GGA(X1, X2, X3, X4, lecC_out_gg(X1, X3)) → MERGEB_IN_GGA(X2, .(X3, X4))
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U5_GGA(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
U5_GGA(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4)
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
gtcD_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)
U5_GGA(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U5_GGA(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
gtcD_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)
U5_GGA(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U5_GGA(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecC_in_gg(x0, x1)
gtcD_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)
lecC_in_gg(x0, x1)
U25_gg(x0, x1, x2)
U5_GGA(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → MERGEB_IN_GGA(.(X1, X2), X4)
MERGEB_IN_GGA(.(X1, X2), .(X3, X4)) → U5_GGA(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
gtcD_in_gg(x0, x1)
U26_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U14_GA(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)), X8)
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6), X9)
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcF_in_ga([], []) → mergesortcF_out_ga([], [])
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4))), X5) → U14_GA(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)), X8)
U14_GA(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
U16_GA(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6), X9)
splitcE_in_gaa([], [], []) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2), .(X1, X3), X4) → U27_gaa(X1, X2, X3, X4, splitcE_in_gaa(X2, X4, X3))
mergesortcF_in_ga(.(X1, .(X2, [])), X3) → U28_ga(X1, X2, X3, mergesortcA_in_ga(X1, X4))
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4))), X5) → U31_ga(X1, X2, X3, X4, X5, splitcE_in_gaa(X4, X6, X7))
U27_gaa(X1, X2, X3, X4, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
U28_ga(X1, X2, X3, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X3, X4, mergesortcA_in_ga(X2, X5))
U31_ga(X1, X2, X3, X4, X5, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_in_ga(.(X1, .(X3, X7)), X8))
mergesortcA_in_ga(X1, .(X1, [])) → mergesortcA_out_ga(X1, .(X1, []))
U29_ga(X1, X2, X3, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, X3, mergecB_in_gga(X4, X5, X3))
U32_ga(X1, X2, X3, X4, X5, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_in_ga(.(X2, X6), X9))
U30_ga(X1, X2, X3, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
U33_ga(X1, X2, X3, X4, X5, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, X5, mergecB_in_gga(X8, X9, X5))
mergecB_in_gga(X1, [], X1) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1, X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U21_gga(X1, X2, X3, X4, X5, lecC_in_gg(X1, X3))
mergecB_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U23_gga(X1, X2, X3, X4, X5, gtcD_in_gg(X1, X3))
mergesortcF_in_ga(.(X1, []), .(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
U34_ga(X1, X2, X3, X4, X5, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
U21_gga(X1, X2, X3, X4, X5, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, X5, mergecB_in_gga(X2, .(X3, X4), X5))
U23_gga(X1, X2, X3, X4, X5, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecB_in_gga(.(X1, X2), X4, X5))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U22_gga(X1, X2, X3, X4, X5, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gga(X1, X2, X3, X4, X5, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4)))) → U14_GA(X1, X2, X3, X4, splitcE_in_gaa(X4))
U14_GA(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)))
U14_GA(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X6, mergesortcF_in_ga(.(X1, .(X3, X7))))
U16_GA(X1, X2, X3, X4, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6))
splitcE_in_gaa([]) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2)) → U27_gaa(X1, X2, splitcE_in_gaa(X2))
mergesortcF_in_ga(.(X1, .(X2, []))) → U28_ga(X1, X2, mergesortcA_in_ga(X1))
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4)))) → U31_ga(X1, X2, X3, X4, splitcE_in_gaa(X4))
U27_gaa(X1, X2, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
U28_ga(X1, X2, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X4, mergesortcA_in_ga(X2))
U31_ga(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X6, mergesortcF_in_ga(.(X1, .(X3, X7))))
mergesortcA_in_ga(X1) → mergesortcA_out_ga(X1, .(X1, []))
U29_ga(X1, X2, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, mergecB_in_gga(X4, X5))
U32_ga(X1, X2, X3, X4, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X8, mergesortcF_in_ga(.(X2, X6)))
U30_ga(X1, X2, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
U33_ga(X1, X2, X3, X4, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, mergecB_in_gga(X8, X9))
mergecB_in_gga(X1, []) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4)) → U21_gga(X1, X2, X3, X4, lecC_in_gg(X1, X3))
mergecB_in_gga(.(X1, X2), .(X3, X4)) → U23_gga(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
mergesortcF_in_ga(.(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
U34_ga(X1, X2, X3, X4, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
U21_gga(X1, X2, X3, X4, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, mergecB_in_gga(X2, .(X3, X4)))
U23_gga(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, mergecB_in_gga(.(X1, X2), X4))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U22_gga(X1, X2, X3, X4, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gga(X1, X2, X3, X4, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa(x0)
mergesortcF_in_ga(x0)
U27_gaa(x0, x1, x2)
U28_ga(x0, x1, x2)
U31_ga(x0, x1, x2, x3, x4)
mergesortcA_in_ga(x0)
U29_ga(x0, x1, x2, x3)
U32_ga(x0, x1, x2, x3, x4, x5)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3, x4, x5)
mergecB_in_gga(x0, x1)
U34_ga(x0, x1, x2, x3, x4)
U21_gga(x0, x1, x2, x3, x4)
U23_gga(x0, x1, x2, x3, x4)
lecC_in_gg(x0, x1)
U22_gga(x0, x1, x2, x3, x4)
gtcD_in_gg(x0, x1)
U24_gga(x0, x1, x2, x3, x4)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGESORTF_IN_GA(.(X1, .(X2, .(X3, X4)))) → U14_GA(X1, X2, X3, X4, splitcE_in_gaa(X4))
U14_GA(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → U16_GA(X1, X2, X3, X4, X6, mergesortcF_in_ga(.(X1, .(X3, X7))))
POL(.(x1, x2)) = 1 + x2
POL(0) = 1
POL(MERGESORTF_IN_GA(x1)) = x1
POL(U14_GA(x1, x2, x3, x4, x5)) = 1 + x5
POL(U16_GA(x1, x2, x3, x4, x5, x6)) = 1 + x5
POL(U21_gga(x1, x2, x3, x4, x5)) = 0
POL(U22_gga(x1, x2, x3, x4, x5)) = 0
POL(U23_gga(x1, x2, x3, x4, x5)) = 0
POL(U24_gga(x1, x2, x3, x4, x5)) = 0
POL(U25_gg(x1, x2, x3)) = 1
POL(U26_gg(x1, x2, x3)) = 0
POL(U27_gaa(x1, x2, x3)) = 1 + x3
POL(U28_ga(x1, x2, x3)) = 0
POL(U29_ga(x1, x2, x3, x4)) = 0
POL(U30_ga(x1, x2, x3)) = 0
POL(U31_ga(x1, x2, x3, x4, x5)) = 0
POL(U32_ga(x1, x2, x3, x4, x5, x6)) = 0
POL(U33_ga(x1, x2, x3, x4, x5, x6)) = 0
POL(U34_ga(x1, x2, x3, x4, x5)) = 0
POL([]) = 0
POL(gtcD_in_gg(x1, x2)) = 0
POL(gtcD_out_gg(x1, x2)) = 0
POL(lecC_in_gg(x1, x2)) = 1 + x1
POL(lecC_out_gg(x1, x2)) = 1
POL(mergecB_in_gga(x1, x2)) = 0
POL(mergecB_out_gga(x1, x2, x3)) = 0
POL(mergesortcA_in_ga(x1)) = 0
POL(mergesortcA_out_ga(x1, x2)) = 0
POL(mergesortcF_in_ga(x1)) = 0
POL(mergesortcF_out_ga(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(splitcE_in_gaa(x1)) = 1 + x1
POL(splitcE_out_gaa(x1, x2, x3)) = 1 + x2 + x3
splitcE_in_gaa([]) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2)) → U27_gaa(X1, X2, splitcE_in_gaa(X2))
U27_gaa(X1, X2, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
U14_GA(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → MERGESORTF_IN_GA(.(X1, .(X3, X7)))
U16_GA(X1, X2, X3, X4, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → MERGESORTF_IN_GA(.(X2, X6))
splitcE_in_gaa([]) → splitcE_out_gaa([], [], [])
splitcE_in_gaa(.(X1, X2)) → U27_gaa(X1, X2, splitcE_in_gaa(X2))
mergesortcF_in_ga(.(X1, .(X2, []))) → U28_ga(X1, X2, mergesortcA_in_ga(X1))
mergesortcF_in_ga(.(X1, .(X2, .(X3, X4)))) → U31_ga(X1, X2, X3, X4, splitcE_in_gaa(X4))
U27_gaa(X1, X2, splitcE_out_gaa(X2, X4, X3)) → splitcE_out_gaa(.(X1, X2), .(X1, X3), X4)
U28_ga(X1, X2, mergesortcA_out_ga(X1, X4)) → U29_ga(X1, X2, X4, mergesortcA_in_ga(X2))
U31_ga(X1, X2, X3, X4, splitcE_out_gaa(X4, X6, X7)) → U32_ga(X1, X2, X3, X4, X6, mergesortcF_in_ga(.(X1, .(X3, X7))))
mergesortcA_in_ga(X1) → mergesortcA_out_ga(X1, .(X1, []))
U29_ga(X1, X2, X4, mergesortcA_out_ga(X2, X5)) → U30_ga(X1, X2, mergecB_in_gga(X4, X5))
U32_ga(X1, X2, X3, X4, X6, mergesortcF_out_ga(.(X1, .(X3, X7)), X8)) → U33_ga(X1, X2, X3, X4, X8, mergesortcF_in_ga(.(X2, X6)))
U30_ga(X1, X2, mergecB_out_gga(X4, X5, X3)) → mergesortcF_out_ga(.(X1, .(X2, [])), X3)
U33_ga(X1, X2, X3, X4, X8, mergesortcF_out_ga(.(X2, X6), X9)) → U34_ga(X1, X2, X3, X4, mergecB_in_gga(X8, X9))
mergecB_in_gga(X1, []) → mergecB_out_gga(X1, [], X1)
mergecB_in_gga([], X1) → mergecB_out_gga([], X1, X1)
mergecB_in_gga(.(X1, X2), .(X3, X4)) → U21_gga(X1, X2, X3, X4, lecC_in_gg(X1, X3))
mergecB_in_gga(.(X1, X2), .(X3, X4)) → U23_gga(X1, X2, X3, X4, gtcD_in_gg(X1, X3))
mergesortcF_in_ga(.(X1, [])) → mergesortcF_out_ga(.(X1, []), .(X1, []))
U34_ga(X1, X2, X3, X4, mergecB_out_gga(X8, X9, X5)) → mergesortcF_out_ga(.(X1, .(X2, .(X3, X4))), X5)
U21_gga(X1, X2, X3, X4, lecC_out_gg(X1, X3)) → U22_gga(X1, X2, X3, X4, mergecB_in_gga(X2, .(X3, X4)))
U23_gga(X1, X2, X3, X4, gtcD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, mergecB_in_gga(.(X1, X2), X4))
lecC_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U22_gga(X1, X2, X3, X4, mergecB_out_gga(X2, .(X3, X4), X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcD_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gga(X1, X2, X3, X4, mergecB_out_gga(.(X1, X2), X4, X5)) → mergecB_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U25_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U26_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
splitcE_in_gaa(x0)
mergesortcF_in_ga(x0)
U27_gaa(x0, x1, x2)
U28_ga(x0, x1, x2)
U31_ga(x0, x1, x2, x3, x4)
mergesortcA_in_ga(x0)
U29_ga(x0, x1, x2, x3)
U32_ga(x0, x1, x2, x3, x4, x5)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3, x4, x5)
mergecB_in_gga(x0, x1)
U34_ga(x0, x1, x2, x3, x4)
U21_gga(x0, x1, x2, x3, x4)
U23_gga(x0, x1, x2, x3, x4)
lecC_in_gg(x0, x1)
U22_gga(x0, x1, x2, x3, x4)
gtcD_in_gg(x0, x1)
U24_gga(x0, x1, x2, x3, x4)
U25_gg(x0, x1, x2)
U26_gg(x0, x1, x2)